(declare-sort c_unique)

(declare-sort c_ssorted)

(declare-sort e)

(declare-fun c_sort (e c_unique) c_ssorted)
(declare-fun f (Int) c_unique)
(declare-fun g (c_ssorted) Int)
(declare-fun h () e)
(declare-fun type_pointer (e) e)
(declare-fun type_alloc_table () e)
(declare-fun block_length (c_ssorted c_ssorted) Int)
(declare-fun j (c_ssorted) Int)
(declare-fun shift (c_ssorted Int) c_unique)
(declare-fun n (c_ssorted c_ssorted) Bool)
(declare-fun type_memory (e e) e)
(declare-fun acc (c_ssorted c_ssorted) c_unique)
(declare-fun ac (c_ssorted c_ssorted c_ssorted) c_unique)
(declare-fun type_pset (e) e)
(declare-fun ad (c_ssorted) c_unique)
(declare-fun bj (c_ssorted Int) c_unique)
(declare-fun s (c_ssorted c_ssorted Int) c_unique)
(declare-fun v (c_ssorted c_ssorted) c_unique)
(declare-fun not_in_pset (c_ssorted c_ssorted) Bool)
(declare-fun t (c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
(declare-fun bn (c_ssorted) Bool)
(declare-fun type_global () e)
(assert (forall ((?i c_unique)) (= (f (g (c_sort h ?i))) ?i)))
(assert (forall ((?k e) (?l c_unique) (?m c_unique)) (let ((?r (c_sort type_alloc_table ?l))(?o (c_sort (type_pointer ?k) ?m))(?aa 0)) (= (n ?r ?o) (< ?aa (block_length ?r ?o))))))
(assert (exists ((?ab e)) (forall ((?p c_unique) (?q c_unique)) (let ((?o (type_pointer ?ab))) (let ((?r (c_sort ?o ?q))) (and (= 0 (j ?r)) (= ?p ?q)))))))
(assert (forall ((?u e) (?y e) (?w c_unique) (?ae c_unique) (?af c_unique)) (let ((?o (type_pointer ?u))) (= (forall ((?ag c_unique)) (let ((?aa (c_sort (type_pointer ?y) ?ag))) (= (= ?af (acc (c_sort (type_memory ?o ?y) ?ae) ?aa)) (not_in_pset ?aa (c_sort (type_pset ?y) ?w))))) (not_in_pset (c_sort (type_pset ?y) ?w) (c_sort (type_memory ?o ?y) ?ae))))))
(assert (forall ((?ah e) (?ai c_unique) (?aj c_unique) (?ak Int)) (let ((?o (type_pset ?ah))) (= (forall ((?al c_unique)) (or (forall ((?am Int)) (= (<= ?ak) (not (= ?ai (shift (c_sort (type_pointer ?ah) ?al) ?am))))))) (not_in_pset (c_sort (type_pointer ?ah) ?ai) (c_sort ?o (bj (c_sort ?o ?aj) ?ak)))))))
(assert (forall ((?an e) (?x e) (?ao c_unique) (?ap c_unique) (?aq c_unique) (?ar Int)) (let ((?o (type_pointer ?x))) (= (forall ((?bk c_unique)) (= (not (not_in_pset (c_sort (type_pointer ?an) ?bk) (c_sort (type_pset ?an) ?ap))) (forall ((?z Int)) (let ((?aa (type_pointer ?an))) (= (= ?ar ?z) (not (= ?ao (acc (c_sort (type_memory ?o ?an) ?aq) (c_sort ?aa (shift (c_sort ?aa ?bk) ?z)))))))))) (not_in_pset (c_sort ?o ?ao) (c_sort (type_pset ?x) (s (c_sort (type_pset ?an) ?ap) (c_sort (type_memory ?o ?an) ?aq) ?ar)))))))
(assert (forall ((?as e) (?bl e) (?at c_unique)) (= (bn (c_sort (type_memory (type_pointer ?bl) ?as) ?at)) (forall ((?bm c_unique) (?bo c_unique)) (let ((?aa (type_pointer ?bl))(?o (c_sort type_alloc_table ?bo))(?r (c_sort (type_pointer ?as) ?bm))) (n ?o (c_sort ?aa (acc (c_sort (type_memory ?aa ?as) ?at) ?r))))))))
(assert (not (forall ((?a c_unique) (?b c_unique) (?c c_unique) (?d c_unique) (?alloc c_unique) (?au c_unique)) (let ((?o (c_sort type_alloc_table ?alloc))(?aa (type_pointer type_global))) (=> and (n ?o (c_sort ?aa ?c)) (forall ((?intM_global0 c_unique)) (let ((?av (c_sort ?aa ?a))(?aw (c_sort ?aa ?b))(?ax (type_memory h type_global))) (let ((?r (c_sort ?ax ?intM_global0))(?ay (c_sort ?ax ?au))(?az type_global)) (=> (t ?o ?ay ?r (c_sort ?az (v (c_sort ?az (ad ?aw)) (c_sort ?az (ad ?av))))) (xor (n ?o (c_sort ?aa ?c)) (forall ((?ba c_unique)) (= (= ?ba (acc ?r (c_sort ?aa ?c))) (forall ((?bb c_unique)) (= (= ?bb (acc ?r (c_sort ?aa ?d))) (forall ((?bc c_unique)) (= (= ?bc (acc ?r (c_sort ?aa ?c))) (forall ((?bd Int)) (=> (= (f ?bd) ?bc) (forall ((?be c_unique)) (=> (n ?o (c_sort ?aa ?c)) (forall ((?bf c_unique)) (=> (= ?bf (ac ?r (c_sort ?aa ?c) (c_sort h ?be))) (forall ((?bg c_unique)) (=> (= ?bg (ac (c_sort ?ax ?bf) (c_sort ?aa ?d) (c_sort h (f ?bd)))) (forall ((?bh c_unique)) (let ((?bi (c_sort ?aa ?bh))) (= ?r ?bi)))))))))))))))))))))))))))
(check-sat)
